open util/integer as integer

abstract sig BasicProduct{
 costs: one Int,
 arrivalPlace: one Location
}{costs > 0}

sig Excursion extends BasicProduct{
 excursionDate : one Int
}

sig Hotel extends BasicProduct{
}

sig Location{}


abstract sig Transportation extends BasicProduct{
departurePlace : one Location
}


sig Bus, Train, Flight extends Transportation{}

sig TravelPackage{
 products : some BasicProduct,
 transportations : some Transportation
}{ //has to contain excatly one hotel
   one h : Hotel | h in products
   no t: Transportation | t in products
   //has to contain exactly two transportations
  #transportations =2
}

sig PersonalizedTravelPackage {
  travelPackage : one TravelPackage,
  departure : one Int,
  return : one Int
}{departure < return 
	departure > 0
	return > 0
}

sig Customer{
  ptps: set PersonalizedTravelPackage
}

fact transportation{
 all t : Transportation | not ( t.departurePlace = t.arrivalPlace)
}

fact noRedundantTP{
 all disj tp1,tp2: TravelPackage | tp1.products != tp2.products or tp1.transportations != tp2.transportations
}

fact sameLocationForAllProductsOfOneTravel{
 all tp : TravelPackage | all disj p1,p2 : tp.products | (p1.arrivalPlace = p2.arrivalPlace)
} 

fact arrivalAndDeparturePlace{
 all tp: TravelPackage | all h : tp.products | some disj de, re: tp.transportations | (h in Hotel) implies (de.arrivalPlace = re.departurePlace and de.arrivalPlace = h.arrivalPlace
 and de.departurePlace = re.arrivalPlace and not (de.arrivalPlace = re.arrivalPlace)) 
}

fact noLocationInstance{
 all l: Location | some b: BasicProduct | l in b.arrivalPlace
}

fact noPTPRelatedToSeveralCustomer{
  all ptp : PersonalizedTravelPackage | one c : Customer | ptp in c.ptps
}


fact noTPRelatedToSeveralPTP{
 all tp : TravelPackage | lone ptp : PersonalizedTravelPackage | tp in ptp.travelPackage
}

fact excursionDateEqualsZeroIfRelatedToAPersonalizedTravelPackage{
 all e : Excursion | all ptp : PersonalizedTravelPackage |all tp : ptp.travelPackage | (e in tp.products) implies ((e.excursionDate < ptp.return) and (e.excursionDate > ptp.departure))
 else (e.excursionDate = 0)
}


assert differentMeanOfTrans{
 no tp: TravelPackage | some t1,t2 : tp.transportations | t1 in Bus and not (t2 in Bus)
}

assert sameMeanOfTrans{
 no tp: TravelPackage | some disj t1,t2 : tp.transportations | (t1 in Flight and t2 in Flight) or (t1 in Bus and t2 in Bus) or (t1 in Train and t2 in Train)
}


//check sameMeanOfTrans
pred show(){

}
run show for  10
